/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.symm;

import java.util.ArrayList;
import java.util.List;

import alloy.bool.BooleanFormula;
import alloy.bool.PartialAssignment;
import alloy.util.Dbg;

/**
 * A symmetry-breaking predicate.  The part of the predicate that
 * consists of setting Boolean variables to particular values
 * is represented explicitly as a {@link PartialAssignment}.
 * This helps in Boolean simplification.
 * The meaning of the predicate is the conjunction of {@link #predicate}
 * and the unit clauses represented by {@link #forcedBoolVars}.
 * This class also provides some convenience methods to aid in the construction
 * of symmetry-breaking predicates.  Note that, unlike {@link BooleanFormula}, this
 * class is mutable.
 */
public class SymmetryBreakingPredicate {
    /** The "general boolean formula" portion of the predicate: set of constraints to conjoin */
    private List /* of BooleanFormula */ _conjuncts = new ArrayList();

    /**
     * The part of the predicate that forces some Boolean variables
     * to specific Boolean values.  This part is kept separately to
     * faciliate Boolean simplification.
     */
    private PartialAssignment _unitClauses = new PartialAssignment();

    //////////////
    // Methods //
    ////////////

    /**
     * Mutate the symmetry-breaking predicate by conjoining the given
     * boolean formula.
     */
    public void conjoin(BooleanFormula conjunct_) {
	if (conjunct_.isLiteral()) {
	    int lit = conjunct_.getLiteral();
	    _unitClauses.setLitValue(lit, true);
	} else
	    _conjuncts.add(conjunct_);
    }

    /**
     * Add a constraint to the symmetry-breaking predicate which forces
     * the truth value of the given {@link BooleanFormula} to the specified
     * Boolean value.
     */
    public void require(BooleanFormula f_, boolean truthValue) {
	conjoin(truthValue ? f_ : f_.not());
    }

    /**
     * Conjoin constraints from the given symmetry-breaking predicate to this symmetry-breaking
     * predicate.
     */
    public void conjoin(SymmetryBreakingPredicate sbp_) {
	_conjuncts.addAll(sbp_._conjuncts);
	for (int boolVar=1; boolVar<=sbp_._unitClauses.getMaxVar(); boolVar++) {
	    if (sbp_._unitClauses.isAssigned(boolVar)) {
		boolean newSetting = sbp_._unitClauses.getVarValue(boolVar);
		if (_unitClauses.isAssigned(boolVar)) {
		    Dbg.chk(_unitClauses.getVarValue(boolVar) == newSetting);
		}
		else {
		    _unitClauses.setVarValue(boolVar, newSetting);
		}
	    }
	}
    }

    /**
     * Return the part of the symmetry-breaking predicate that is expressed as a general
     * Boolean constraint.
     * @see #getUnitClauses
     */
    public BooleanFormula getConjuncts() { return  BooleanFormula.makeAnd(_conjuncts); }

    /**
     * Return the part of the symmetry-breaking predicate that is explicitly expressed
     * as a collection of unit clauses.
     */
    public PartialAssignment getUnitClauses() { return _unitClauses; }

    /**
     * Return the entire symmetry-breaking predicate as one formula.
     */
    public BooleanFormula getSymmBrkPredicate() {
	List /* of BooleanFormula */ conjuncts = new ArrayList(_conjuncts);
	// convert the partial assignment to a conjunction of literals
	for (int boolVar=1; boolVar<=_unitClauses.getMaxVar(); boolVar++) {
	    if (_unitClauses.isAssigned(boolVar)) {
		boolean val = _unitClauses.getVarValue(boolVar);
		conjuncts.add(BooleanFormula.makeLit(val ? boolVar : -boolVar));
	    }
	}
	return BooleanFormula.makeAnd(conjuncts);
    }

    public String toString() {
	return "[unit clauses: " + _unitClauses + "]";
    }
}
